Termination w.r.t. Q proof of TRS/ThiemannmapHard.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

AP₂(ap₂(map, f), xs) -> AP₂(ap₂(if, ap₂(isEmpty, xs)), f)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(last, xs)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(f, ap₂(last, xs))
AP₂(ap₂(map, f), xs) -> AP₂(if, ap₂(isEmpty, xs))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
AP₂(ap₂(map, f), xs) -> AP₂(isEmpty, xs)
AP₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(last, ap₂(ap₂(cons, y), ys))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(map, f), ap₂(dropLast, xs))
AP₂(ap₂(map, f), xs) -> AP₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(map, f)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(cons, ap₂(f, ap₂(last, xs)))
AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(dropLast, ap₂(ap₂(cons, y), ys))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(dropLast, xs)
AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

AP₂(ap₂(map, f), xs) -> AP₂(ap₂(if, ap₂(isEmpty, xs)), f)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(last, xs)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(f, ap₂(last, xs))
AP₂(ap₂(map, f), xs) -> AP₂(if, ap₂(isEmpty, xs))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
AP₂(ap₂(map, f), xs) -> AP₂(isEmpty, xs)
AP₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(last, ap₂(ap₂(cons, y), ys))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(map, f), ap₂(dropLast, xs))
AP₂(ap₂(map, f), xs) -> AP₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(map, f)
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(cons, ap₂(f, ap₂(last, xs)))
AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(dropLast, ap₂(ap₂(cons, y), ys))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(dropLast, xs)
AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 9 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(dropLast, ap₂(ap₂(cons, y), ys))

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

AP₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(dropLast, ap₂(ap₂(cons, y), ys))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(AP₂(x₁, x₂)) = 2·x₂
POL(ap₂(x₁, x₂)) = 2 + 3·x₂
POL(cons) = 0
POL(dropLast) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(last, ap₂(ap₂(cons, y), ys))

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

AP₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> AP₂(last, ap₂(ap₂(cons, y), ys))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(AP₂(x₁, x₂)) = 2·x₂
POL(ap₂(x₁, x₂)) = 2 + 3·x₂
POL(cons) = 0
POL(last) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(f, ap₂(last, xs))
AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(map, f), ap₂(dropLast, xs))
AP₂(ap₂(map, f), xs) -> AP₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(f, ap₂(last, xs))

The remaining pairs can at least be oriented weakly.

AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(map, f), ap₂(dropLast, xs))
AP₂(ap₂(map, f), xs) -> AP₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)

Used ordering: Polynomial interpretation [21]:

POL(AP₂(x₁, x₂)) = 2·x₁
POL(ap₂(x₁, x₂)) = 2 + 2·x₂
POL(cons) = 0
POL(dropLast) = 0
POL(false) = 3
POL(if) = 0
POL(isEmpty) = 0
POL(last) = 0
POL(map) = 0
POL(nil) = 3
POL(true) = 3

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

AP₂(ap₂(ap₂(if, false), f), xs) -> AP₂(ap₂(map, f), ap₂(dropLast, xs))
AP₂(ap₂(map, f), xs) -> AP₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)

The TRS R consists of the following rules:

ap₂(ap₂(map, f), xs) -> ap₂(ap₂(ap₂(if, ap₂(isEmpty, xs)), f), xs)
ap₂(ap₂(ap₂(if, true), f), xs) -> nil
ap₂(ap₂(ap₂(if, false), f), xs) -> ap₂(ap₂(cons, ap₂(f, ap₂(last, xs))), ap₂(ap₂(map, f), ap₂(dropLast, xs)))
ap₂(isEmpty, nil) -> true
ap₂(isEmpty, ap₂(ap₂(cons, x), xs)) -> false
ap₂(last, ap₂(ap₂(cons, x), nil)) -> x
ap₂(last, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(last, ap₂(ap₂(cons, y), ys))
ap₂(dropLast, nil) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), nil)) -> nil
ap₂(dropLast, ap₂(ap₂(cons, x), ap₂(ap₂(cons, y), ys))) -> ap₂(ap₂(cons, x), ap₂(dropLast, ap₂(ap₂(cons, y), ys)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.